w:World, e:(Id). w-pred(w;e)  E+Unit 

latex

Definitions	Type, x.A(x), x. t(x), #$n, AB, n-m, -n, n+m, a<b, Void, x:AB(x), P  Q, False, , S  T, inl(x), b, , s = t, Prop, P & Q, P  Q, false, i=j, , inr(x), E, World, ij, <a,b>, w-pred(w;e), Unit, 2of(t), 1of(t), a(i;t), isnull(a), b, A, , Id, x:AB(x), {x:A| B(x) }, left+right, t  T, x:A. B(x)
Lemmas	ge wf, nat properties, world wf, it wf, not functionality wrt iff, assert of eq int, eq int wf, bfalse wf, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, bool wf, bnot wf, unit wf, le wf, not wf, assert wf, w-isnull wf, w-a wf, pi1 wf, pi2 wf, nat wf, Id wf